PRISM
=====
Version: 4.5.dev
Date: Sun Mar 15 03:30:39 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -mtbdd -e 1e-6 -maxiters 1000000 zeroconf-pta.prism zeroconf-pta.props --property incorrect -const T=200
Parsing model file "zeroconf-pta.prism"...
Type: PTA
Modules: sender environment
Variables: s probes ip x e y
Parsing properties file "zeroconf-pta.props"...
2 properties:
(1) "deadline": Pmax=? [ F<=T s=2&ip=2 ]
(2) "incorrect": Pmax=? [ F s=2&ip=2 ]
---------------------------------------------------------------------
Model checking: "incorrect": Pmax=? [ F s=2&ip=2 ]
Building PTA...
PTA: 2 clocks, 23 locations, 26 transitions
Target (s=2&ip=2) satisfied by 3 locations.
Building initial STPG...
Building forwards reachability graph... 27 states
Graph constructed in 0.018 secs.
Graph: 27 symbolic states (1 initial, 2 target)
Model checking STPG...
STPG model checked in 0.02 secs.
27/27 states converged.
Diff across 1 initial state: 9.068567511510972E-12
Lower/upper bounds for 1 initial state: 0.00130151379208389 - 0.0013015138011524575
Initial STPG: 27 states (1 initial), 38 transitions, 26 choices, 25 choice sets, p1max/avg = 1/0.93, p2max/avg = 2/1.04
Final STPG: 27 states (1 initial), 38 transitions, 26 choices, 25 choice sets, p1max/avg = 1/0.93, p2max/avg = 2/1.04
Terminated after 0 refinements in 0.10 secs.
Abstraction-refinement time breakdown:
* 0.06 secs (64.6%) = Building initial STPG
* 0.00 secs (0.0%) = Rebuilding STPG (0 x avg 0.00 secs)
* 0.02 secs (20.8%) = model checking STPG (1 x avg 0.02 secs) (lb=89.5%) (prob0=25.0%) (pre=60.0%) (iters=112)
* 0.00 secs (0.0%) = refinement (0 x avg 0.00 secs)
Final diff across 1 initial state: 9.068567511510972E-12
Final lower/upper bounds for 1 initial state: 0.00130151379208389 - 0.0013015138011524575
Model checking completed in 0.184 secs.
Result (maximum probability): 0.0013015137966181738
Overall running time: 0.686 seconds.